Inference at * 
Iof proof for Lemma last-not-before:


  T:Type, L:(T List).
  ((null(L)))  no_repeats(T;L)  (x:T. last(L) before x  L  False) 

latex

 by ((((Auto) 
CollapseTHEN (((((InstLemma `no_repeats_iff` [T;L]) 
THENM (((ThinTrivial) 

THECollapseTHEN (Thin (-2)))))) 
TCollapseTHENA (Auto))))) 
TCollapseTHEN (((FHyp (-1) [-2]) 

TCoCollapseTHENA (Auto)))) 

latex

TC1: 

TC1: 1. T : Type
TC1: 2. L : T List
TC1: 3. (null(L))
TC1: 4. no_repeats(T;L)
TC1: 5. x : T
TC1: 6. last(L) before x  L
TC1: 7. x, y:T. x before y  L  ((x = y))
TC1: 8. (last(L) = x)
TC1:   False
TC.

Definitions	False, b, null(as), S  T, Top, x:A.B(x), Void, P  Q, P & Q, x:A  B(x), P  Q, x before y  l, no_repeats(T;l), A, type List, Type, last(L), x:A. B(x), P  Q, x:AB(x), t  T, s = t
Lemmas	l before wf, false wf, no repeats wf, not wf, assert wf, null wf3, member wf, top wf, no repeats iff, last wf